YES(?,O(n^2))

We are left with following problem, upon which TcT provides the
certificate YES(?,O(n^2)).

Strict Trs:
  { if(true(), t, e) -> t
  , if(false(), t, e) -> e
  , member(x, []()) -> false()
  , member(x, ::(y, ys)) -> if(eq(x, y), true(), member(x, ys))
  , eq([](), []()) -> true()
  , eq(O(x), O(y)) -> eq(x, y)
  , eq(O(x), 1(y)) -> false()
  , eq(1(x), O(y)) -> false()
  , eq(1(x), 1(y)) -> eq(x, y)
  , negate(1(x)) -> 0(x)
  , negate(0(x)) -> 1(x)
  , choice(::(x, xs)) -> x
  , choice(::(x, xs)) -> choice(xs)
  , guess([]()) -> []()
  , guess(::(clause, cnf)) -> ::(choice(clause), guess(cnf))
  , verify([]()) -> true()
  , verify(::(l, ls)) ->
    if(member(negate(l), ls), false(), verify(ls))
  , sat(cnf) -> satck(cnf, guess(cnf))
  , satck(cnf, assign) -> if(verify(assign), assign, unsat()) }
Obligation:
  innermost runtime complexity
Answer:
  YES(?,O(n^2))

The following argument positions are usable:
  Uargs(if) = {1, 3}, Uargs(member) = {1}, Uargs(::) = {1, 2},
  Uargs(satck) = {2}

TcT has computed following constructor-based matrix interpretation
satisfying not(EDA).

            [true] = [1]
                     [0]
                        
  [if](x1, x2, x3) = [1 0] x1 + [1 0] x2 + [1 0] x3 + [0]
                     [0 0]      [0 1]      [0 2]      [0]
                                                         
           [false] = [1]
                     [0]
                        
              [[]] = [2]
                     [2]
                        
  [member](x1, x2) = [1 0] x1 + [1 0] x2 + [0]
                     [0 0]      [0 0]      [0]
                                              
      [::](x1, x2) = [1 0] x1 + [1 0] x2 + [2]
                     [1 1]      [1 1]      [2]
                                              
      [eq](x1, x2) = [1 0] x2 + [0]
                     [0 0]      [0]
                                   
           [O](x1) = [1 0] x1 + [2]
                     [0 0]      [0]
                                   
           [1](x1) = [1 0] x1 + [2]
                     [0 0]      [2]
                                   
           [0](x1) = [0 0] x1 + [2]
                     [1 0]      [2]
                                   
      [negate](x1) = [1 1] x1 + [0]
                     [2 0]      [0]
                                   
      [choice](x1) = [1 0] x1 + [0]
                     [0 1]      [0]
                                   
       [guess](x1) = [2 0] x1 + [0]
                     [0 2]      [0]
                                   
      [verify](x1) = [0 1] x1 + [0]
                     [0 0]      [0]
                                   
         [sat](x1) = [2 2] x1 + [2]
                     [1 2]      [2]
                                   
   [satck](x1, x2) = [0 0] x1 + [1 1] x2 + [1]
                     [1 0]      [0 1]      [2]
                                              
           [unsat] = [0]
                     [0]

This order satisfies following ordering constraints

        [if(true(), t, e)] = [1 0] t + [1 0] e + [1]                         
                             [0 1]     [0 2]     [0]                         
                           > [1 0] t + [0]                                   
                             [0 1]     [0]                                   
                           = [t]                                             
                                                                             
       [if(false(), t, e)] = [1 0] t + [1 0] e + [1]                         
                             [0 1]     [0 2]     [0]                         
                           > [1 0] e + [0]                                   
                             [0 1]     [0]                                   
                           = [e]                                             
                                                                             
         [member(x, []())] = [1 0] x + [2]                                   
                             [0 0]     [0]                                   
                           > [1]                                             
                             [0]                                             
                           = [false()]                                       
                                                                             
    [member(x, ::(y, ys))] = [1 0] x + [1 0] y + [1 0] ys + [2]              
                             [0 0]     [0 0]     [0 0]      [0]              
                           > [1 0] x + [1 0] y + [1 0] ys + [1]              
                             [0 0]     [0 0]     [0 0]      [0]              
                           = [if(eq(x, y), true(), member(x, ys))]           
                                                                             
          [eq([](), []())] = [2]                                             
                             [0]                                             
                           > [1]                                             
                             [0]                                             
                           = [true()]                                        
                                                                             
          [eq(O(x), O(y))] = [1 0] y + [2]                                   
                             [0 0]     [0]                                   
                           > [1 0] y + [0]                                   
                             [0 0]     [0]                                   
                           = [eq(x, y)]                                      
                                                                             
          [eq(O(x), 1(y))] = [1 0] y + [2]                                   
                             [0 0]     [0]                                   
                           > [1]                                             
                             [0]                                             
                           = [false()]                                       
                                                                             
          [eq(1(x), O(y))] = [1 0] y + [2]                                   
                             [0 0]     [0]                                   
                           > [1]                                             
                             [0]                                             
                           = [false()]                                       
                                                                             
          [eq(1(x), 1(y))] = [1 0] y + [2]                                   
                             [0 0]     [0]                                   
                           > [1 0] y + [0]                                   
                             [0 0]     [0]                                   
                           = [eq(x, y)]                                      
                                                                             
            [negate(1(x))] = [1 0] x + [4]                                   
                             [2 0]     [4]                                   
                           > [0 0] x + [2]                                   
                             [1 0]     [2]                                   
                           = [0(x)]                                          
                                                                             
            [negate(0(x))] = [1 0] x + [4]                                   
                             [0 0]     [4]                                   
                           > [1 0] x + [2]                                   
                             [0 0]     [2]                                   
                           = [1(x)]                                          
                                                                             
       [choice(::(x, xs))] = [1 0] x + [1 0] xs + [2]                        
                             [1 1]     [1 1]      [2]                        
                           > [1 0] x + [0]                                   
                             [0 1]     [0]                                   
                           = [x]                                             
                                                                             
       [choice(::(x, xs))] = [1 0] x + [1 0] xs + [2]                        
                             [1 1]     [1 1]      [2]                        
                           > [1 0] xs + [0]                                  
                             [0 1]      [0]                                  
                           = [choice(xs)]                                    
                                                                             
             [guess([]())] = [4]                                             
                             [4]                                             
                           > [2]                                             
                             [2]                                             
                           = [[]()]                                          
                                                                             
  [guess(::(clause, cnf))] = [2 0] cnf + [2 0] clause + [4]                  
                             [2 2]       [2 2]          [4]                  
                           > [2 0] cnf + [1 0] clause + [2]                  
                             [2 2]       [1 1]          [2]                  
                           = [::(choice(clause), guess(cnf))]                
                                                                             
            [verify([]())] = [2]                                             
                             [0]                                             
                           > [1]                                             
                             [0]                                             
                           = [true()]                                        
                                                                             
       [verify(::(l, ls))] = [1 1] l + [1 1] ls + [2]                        
                             [0 0]     [0 0]      [0]                        
                           > [1 1] l + [1 1] ls + [1]                        
                             [0 0]     [0 0]      [0]                        
                           = [if(member(negate(l), ls), false(), verify(ls))]
                                                                             
                [sat(cnf)] = [2 2] cnf + [2]                                 
                             [1 2]       [2]                                 
                           > [2 2] cnf + [1]                                 
                             [1 2]       [2]                                 
                           = [satck(cnf, guess(cnf))]                        
                                                                             
      [satck(cnf, assign)] = [0 0] cnf + [1 1] assign + [1]                  
                             [1 0]       [0 1]          [2]                  
                           > [1 1] assign + [0]                              
                             [0 1]          [0]                              
                           = [if(verify(assign), assign, unsat())]           
                                                                             

Hurray, we answered YES(?,O(n^2))